from bs4 import BeautifulSoup
import re
from .models import Structure
from django.http import HttpResponse, HttpResponseRedirect, HttpRequest

def add_Theory_synopsis(soup):
    # url = '/home/satone/HOL/help/src-sml/htmlsigs/' + theory + '.html'
    contentD = {}
    # if theory:
    #     try:
    #         soup = BeautifulSoup(open(url), "html.parser")
    #     except:
    #         return False
    content = re.findall(r'\(\*.*?\*\)', soup.text.replace('\n', '%'))[-1][2:-2]
    # content = re.sub(r'\].*?⊢\s+', '] ⊢ ', content)
    content = re.sub(r'\%\s+\[', '||[', content)
    contentL = content.replace('%', ' ').split('||')
    for each in contentL:
        if each.find('Theorem') > 0:
            each = re.sub(r'\s+', ' ', each)
            contentD[each[1:each.find('Theorem')-2]] = each[each.find('Theorem')-1:]
        elif each.find('Definition') > 0:
            each = re.sub(r'\s+', ' ', each)
            contentD[each[1:each.find('Definition')-2]] = each[each.find('Definition')-1:].strip()
    return contentD

def add_Theory(StructureDB, TheoryDB, structure):
    if structure:
        url = '/home/satone/HOL/help/src-sml/htmlsigs/' + structure + '.html'
        try:
            soup = BeautifulSoup(open(url), "html.parser")
        except:
            return False
        try:
            source = soup.table.a['href']
        except:
            source = ''
        if not StructureDB.objects.filter(name=structure).exists():
            stu = StructureDB(name=structure, url=url, source=source)
            stu.save()
        else:
            stu = StructureDB.objects.get(name=structure)
        try:
            pre = soup.find('pre')
            b = pre.text
            b = b.replace('\n', '  ')
            b = re.sub(r'\(\*.*?\*\)', '', b)
            b = re.sub(r'\s+->\s+', ' -> ', b)
        except:
            print ('!!error!!\nfilename:%s'%url)
            return False
        len1 = len(b)
        indexFix = 0
        for x in re.finditer(r'\{.*?\}', b):
            c = re.sub(r'\s+', ' ', b[x.span()[0]-indexFix:x.span()[1]-indexFix])
            b = b[:x.span()[0]-indexFix] + c + b[x.span()[1]-indexFix:]
            indexFix = len1 - len(b)
        # b = pre.text.replace('&gt;\n', '&gt;').replace('\n', '  ')
        # splitResult = []
        try:
            contentD = add_Theory_synopsis(soup)
        except Exception as e:
            contentD = {}
            print(e)
        if b.find(' val ') > 0:
            try:
                # while b.find('(*') > 0:
                #     b = b[:b.find('(*')] + b[b.find('*)')+len('*)'):]
                b = b[b.find(' val '):]
                while b[5:].find(' val ') > 0:
                    t = b[:b[5:].find(' val ') + 5]
                    # splitResult.append({'name': t[5:t.find(':')].strip(), 'type': t[t.find(':')+1:].strip()})
                    if not TheoryDB.objects.filter(name=t[5:t.find(':')].strip(), structure=stu).exists():
                        if t.find('=') > 0 and t.find('=') < t.find(':'):
                            pass
                        else:
                            name = t[5:t.find(':')].strip()
                            ttype = t[t.find(':')+1:].lstrip()
                            if ttype.find(';') > 0 and ttype.find(';') < ttype.find('  '):
                                right = ttype.find(';')
                            else:
                                right = ttype.find('  ')
                            tac = TheoryDB(name=name, type=ttype[:right].rstrip(), structure=stu)
                            #print("save:%s"%name)
                            tac.save()
                    b = b[b[5:].find(' val ') + 5:]
                else:
                    t = b[:b.find('end')]
                    # splitResult.append({'name': t[5:t.find(':')].strip(), 'type': t[t.find(':')+1:].strip()})
                    if not TheoryDB.objects.filter(name=t[5:t.find(':')].strip(), structure=stu).exists():
                        if t.find('=') > 0 and t.find('=') < t.find(':'):
                            pass
                        else:
                            # tac = Theory(name=t[5:t.find(':')].strip(), type=t[t.find(':')+1:t.find('  ')].strip(), structure=stu)
                            # tac.save()
                            name = t[5:t.find(':')].strip()
                            ttype = t[t.find(':')+1:].lstrip()
                            if ttype.find(';') > 0 and ttype.find(';') < ttype.find('  '):
                                right = ttype.find(';')
                            else:
                                right = ttype.find('  ')
                            tac = TheoryDB(name=name, type=ttype[:right].rstrip(), structure=stu)
                            #print("save:%s"%name)
                            tac.save()

                c = pre.find_all('a')
                for each in c:
                    try:
                        TheoryDB.objects.filter(name=each.text, structure=stu).update(url=each['href'], synopsis=contentD[each.text].strip())
                    except:
                        continue
                return True
            except Exception as e:
                print ('!!error:%s!!\nname:%s\ntype:%s\nstruture:%s'%(e, t[5:t.find(':')].strip(),t[t.find(':')+1:t.find('  ')].strip(),structure))
                return False
        else:
            return False
                
            #integrationTheory
            #real_topologyTheory

CREEP_VER = 'v0.2.3'

def char_change_1(x, inline=lambda x: x, outline=lambda x: x):
    flag = 0
    result = ""
    inlines = ""
    outlines = ""
    ctype = 0
    for count,char in enumerate(x):
        if char == '{':
            flag += 1
            if flag == 1:
                char = ''
        elif char == '}':
            flag -= 1
        if flag >= 1:
            inlines += char
            if char == '\n':
                ctype = 1
        else:
            if inlines:
                inlines = inline(inlines)
                outlines = outline(outlines)
                if ctype == 1:
                    result += outlines + "{*%s*}"%inlines
                else:
                    result += outlines + "%*{}*%".format(inlines)
                inlines = ""
                outlines = ""
                ctype = 0
            else:
                outlines += char
    result += outline(outlines)
    return result

import os
def update_from_doc_file(eachFile, path="/home/satone/HOL/help/Docfiles"):
    #docFiles = os.listdir(path)
    attributes = ['STRUCTURE', 'SYNOPSIS', 'LIBRARY', 'DESCRIPTION', 'FAILURE', 'EXAMPLE', 'COMMENTS', 'USES', 'SEEALSO', 'DOC', 'TYPE', 'DESCRIBE', 'ENDDOC', 'KEYWORDS']
    result = {}
    #for eachFile in docFiles:
    if eachFile[-4:] != ".doc":
        eachFile += '.doc'
    if os.path.isfile(os.path.join(path, eachFile)):
        f = open(os.path.join(path, eachFile), 'r')
        b = f.read()
        f.close()
        # b = re.sub('{(?P<funciton>.*?)}', lambda x : "%*{}*%".format(x.group('funciton').replace('\n', '/n\\').replace(' ', '/b\\')), b)
        # b = re.sub('{(?P<funciton>[\s\S]*?)}', lambda x : "{*%s*}"%x.group('funciton').replace('\n', '/n\\').replace(' ', '/b\\'), b)
        # b = ' ' + re.sub('\s\s+', '\n', re.sub('\s', ' ', b)).replace('/n\\', '\n').replace('/b\\', ' ')
        b = ' ' + b.replace('\BLTYPE\n', '\TYPE\n{').replace('\n\ELTYPE', '}')
        for x in attributes:
            if re.search('\\\%s'%x, b) and re.search('\\\%s'%x, b).span()[0] >= 0:
                result[x] = re.search('\\\%s'%x, b).span()[0]
            else:
                result[x] = 0
        attributes = [x[0] for x in sorted(result.items(), key=lambda x: x[1], reverse=True)]
        for x in attributes:
            if re.search('\\\%s'%x, b) and re.search('\\\%s'%x, b).span()[0] >= 0:
                result[x] = b[re.search('\\\%s'%x, b).span()[1]:].strip()
                if x != 'TYPE':
                    #result[x] = re.sub('{(?P<funciton>.*?)}', lambda x : "%*{}*%".format(x.group('funciton').replace('\n', '/n\\').replace(' ', '/b\\')), result[x])
                    #result[x] = re.sub('{(?P<funciton>(?<=\{).*(?=\}))}', lambda x : "%*{}*%".format(x.group('funciton').replace('\n', '/n\\').replace(' ', '/b\\')), result[x])
                    result[x] = char_change_1(result[x], inline=lambda x: x.replace('\n', '/n\\').replace(' ', '/b\\'))
                    #result[x] = re.sub('{(?P<funciton>[\s\S]*?)}', lambda x : "{*%s*}"%x.group('funciton').replace('\n', '/n\\').replace(' ', '/b\\').replace('%*', '{').replace('*%', '}'), result[x])
                    #result[x] = re.sub('{(?P<funciton>(?<=\{)[\s\S]*(?=\}))}', lambda x : "{*%s*}"%x.group('funciton').replace('\n', '/n\\').replace(' ', '/b\\').replace('%*', '{').replace('*%', '}'), result[x])
                    result[x] = re.sub('\s\s+', '\n', re.sub('\s', ' ', result[x])).replace('/n\\', '\n').replace('/b\\', ' ')
                b = b[:re.search('\\\%s'%x, b).span()[0]]
            else:
                result[x] = None
        if not result['STRUCTURE'] or result['STRUCTURE'] != eachFile[:-4].split('.')[0]:
            result['STRUCTURE'] = eachFile[:-4].split('.')[0]
            result['NAME'] = eachFile[:-4].split('.')[1]
        if result['LIBRARY'] and result['LIBRARY'] != result['STRUCTURE']:
            result['SYNOPSIS'] += '\n%%* LIBRARY: %s *%%'%result['LIBRARY']
        if result['KEYWORDS']:
            result['SYNOPSIS'] += '\nkeywords: %s'%result['KEYWORDS']
        try:
            result['TYPE'] = result['TYPE'][result['TYPE'].find(result['NAME'])+len(result['NAME'])+2:-1].strip()
        except:
            result['TYPE'] = result['TYPE'].split('=')[1][:-1].strip()
        if not result['DESCRIPTION']:
            result['DESCRIPTION'] = result['DESCRIBE']
            result['DESCRIBE'] = None
        if result['SEEALSO']:
            seealsoDir = {}
            for each in result['SEEALSO'].split(','):
                try:
                    c = each.split('.')
                    seealsoDir[c[1].strip()] = os.path.join(path, "%s.%s.doc"%(c[0].strip(), c[1].strip()))
                except:
                    continue
            result['SEEALSO'] = seealsoDir
        result['DATATIME'] = os.stat(os.path.join(path, eachFile)).st_mtime
        result['URL'] = 'file://' + os.path.join(path, 'HTML', eachFile[:-3]) + "html"
    return result


